(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
Bit-reversal rev(x)
From the book "Hacker's delight" by Henry S. Warren, Jr., page 101
We verify rev(rev(x)) = x

Contributed by Robert Brummayer (robert.brummayer@gmail.com)
|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun x () (_ BitVec 2048))
(assert (let ((?v_0 ((_ zero_extend 2037) (_ bv1 11)))) (let ((?v_1 (bvor (bvshl (bvand x (_ bv10772335357103669100238292229556650653481367556571828010710115142508218379622630297732400470507637821229572653640632673164706519716830307031696050795482761040210292455766998697250065916796550702265352546128022522758930739547539918720612698112825390156860548617345435014295858630513688602869184133041310128507304777796556114140228324928854856498285392011775440686025935219777008730902820104716752864288059038908647867906153952452532783717433881968134565871077762410409041894903606736575052367242310441156559514193552232645015332422784332879405175055463145778514534045144409868215106159534984049397851951203686532076885 2048)) ?v_0) (bvlshr (bvand x (_ bv21544670714207338200476584459113301306962735113143656021420230285016436759245260595464800941015275642459145307281265346329413039433660614063392101590965522080420584911533997394500131833593101404530705092256045045517861479095079837441225396225650780313721097234690870028591717261027377205738368266082620257014609555593112228280456649857709712996570784023550881372051870439554017461805640209433505728576118077817295735812307904905065567434867763936269131742155524820818083789807213473150104734484620882313119028387104465290030664845568665758810350110926291557029068090288819736430212319069968098795703902407373064153770 2048)) ?v_0))) (?v_2 ((_ zero_extend 2037) (_ bv2 11)))) (let ((?v_3 (bvor (bvshl (bvand ?v_1 (_ bv6463401214262201460142975337733990392088820533943096806426069085504931027773578178639440282304582692737743592184379603898823911830098184219017630477289656624126175473460199218350039550077930421359211527676813513655358443728523951232367618867695234094116329170407261008577515178308213161721510479824786077104382866677933668484136994957312913898971235207065264411615561131866205238541692062830051718572835423345188720743692371471519670230460329180880739522646657446245425136942164041945031420345386264693935708516131339587009199453670599727643105033277887467108720427086645920929063695720990429638711170722211919246131 2048)) ?v_2) (bvlshr (bvand ?v_1 (_ bv25853604857048805840571901350935961568355282135772387225704276342019724111094312714557761129218330770950974368737518415595295647320392736876070521909158626496504701893840796873400158200311721685436846110707254054621433774914095804929470475470780936376465316681629044034310060713232852646886041919299144308417531466711734673936547979829251655595884940828261057646462244527464820954166768251320206874291341693380754882974769485886078680921841316723522958090586629784981700547768656167780125681381545058775742834064525358348036797814682398910572420133111549868434881708346583683716254782883961718554844682888847676984524 2048)) ?v_2))) (?v_4 ((_ zero_extend 2037) (_ bv4 11)))) (let ((?v_5 (bvor (bvshl (bvand ?v_3 (_ bv1901000357135941605924404511098232468261417804100910825419432083972038537580464170188070671266053733158159880054229295264359974067675936535005185434496957830625345727488293887750011632375861888635062214022592209898634836390742338597755182019910362968857743873649194414287504464208297988741620729360231199148347901964098137789452057340386151146756245649136842474004576803490060364276968253773544623109657477454467270806968344550446961832488332112023746918425487484189830922630048247630891594219231254321745796622391570466767411604020764625777383833317025725620211890319601741449724616388526596952562109035944682131215 2048)) ?v_4) (bvlshr (bvand ?v_3 (_ bv30416005714175065694790472177571719492182684865614573206710913343552616601287426723009130740256859730530558080867668724229759585082814984560082966951951325290005531639812702204000186118013790218160995424361475358378157382251877417564082912318565807501723901978387110628600071427332767819865931669763699186373566431425570204631232917446178418348099930386189479584073228855840965828431492060376713969754519639271476332911493512807151389319813313792379950694807799747037294762080771962094265507507700069147932745958265127468278585664332234012438141333072411609923390245113627863195593862216425551240993744575114914099440 2048)) ?v_4))) (?v_6 ((_ zero_extend 2037) (_ bv8 11)))) (let ((?v_7 (bvor (bvshl (bvand ?v_5 (_ bv125747105335840495333520920967587361713790282761538848374048036682975311824388680518277048293863476512407462882964583733440153926655606696868047285550382424593894464464206210473736178017080358392202558904218161744267674002500465977283416709488234126344675664793915583824465275842572240500418491825384943134326514915913106390741964882437994433832125198581036272599524535639420335380188561533658593746553218353019235812134092830185207592032302124141648628845265709070922668033894242061187381718781833943461784212376096100914575864857404663961928113487896643328963432433592333092005130266945339098029400208603344732415 2048)) ?v_6) (bvlshr (bvand ?v_5 (_ bv32191258965975166805381355767702364598730312386953945183756297390841679827043502212678924363229049987176310498038933435760679405223835314398220105100897900696036982902836789881276461572372571748403855079479849406532524544640119290184554677628987936344236970187242389459063110615698493568107133907298545442387587818473755236029943009904126575061024050836745285785478281123691605857328271752616599999117623898372924367906327764527413143560269343780262048984388021522156203016676925967663969720008149489526216758368280601834131421403495593974253597052901540692214638702999637271553313348338006809095526453402456251498240 2048)) ?v_6))) (?v_8 ((_ zero_extend 2037) (_ bv16 11)))) (let ((?v_9 (bvor (bvshl (bvand ?v_7 (_ bv493110854499153261527303304830400414429163719268741078049504027152977022733232996524058187154171131783400490729235363527383303464462683996751272600003788441958449080173047226631524142856549004482903667216748822318336088295811827763886630366639854898310597766941366022901377479767781036797649456019102650190303406219229875374531714524414675213922763874381285717351691497311915806227145891849646132610039780837175085886117183535370834050266286920432789075075656304548989512561008593767263638886841499053506851741469043409601385435225185752143301114887612147878963061101869624862983024529730566675214853496666914815 2048)) ?v_8) (bvlshr (bvand ?v_7 (_ bv32316512960456508147453349385365121560029673505996215291052295923497502161845157660200677353335759292556934560431168784130592175847026458411091401113848279332188918918220823044523566226246795557791574734716850819454473882554323944334074207708109530615683335254269363676864674514061298027570754749667911282871724029983449112545310443072040154819642253271451940772360453967833714276902233168258408946731567076945106428632575740174062980318251379617483264824158211574922576695198259201131389838088044481970625035728915228891636395882917773452463381865274549723395723172372127735020455495580422417626880638757562929315840 2048)) ?v_8))) (?v_10 ((_ zero_extend 2037) (_ bv32 11)))) (let ((?v_11 (bvor (bvshl (bvand ?v_9 (_ bv7524389322797446040883062092537733229786709286255942365591042456667314442386984930096710212860769417795340657030827683038844698134727362301284631268392235937583875243951827485067390432889168540459798904583851961347493402961438138317409892571406969311454956545629852567160903318873644454808418626039175260691609949036049282500668357192980174976837821551246685093927923721588007749784843196246171229662840693970933302712516988312146012401244517765743466989949769396632294237631961231141629598705401114366081875798891955552658541527505604808849729680814712227957530391280469301474478369841928076546552539119615 2048)) ?v_10) (bvlshr (bvand ?v_9 (_ bv32317006063786617977917430647786889867906369439928774745874403061933612682200576450810216481426203250827948543126557362463291876111646222960360790085163651852238641429717120847798370265322261673906889097924268663692940257295126353200399956021066277899174676540581348497257723324380162489733907944315511759482739072698058393384635692285896212301876001058488500506831120565403102471120452564365415396618005887063102909747528554645081362840155633503159179847489820241277356288078525972093195870585301724764277428214574822136154041715694457110709920357539707654728889907475699213364849177130473778351627777064507057111040 2048)) ?v_10))) (?v_12 ((_ zero_extend 2037) (_ bv64 11)))) (let ((?v_13 (bvor (bvshl (bvand ?v_11 (_ bv1751908409537131537125538500170898456289982643253648994597171622084866540056922972656596711067189883143022427928261387198048309577447708096161081508699543188141910799902361070622401213741372869165576561922289064005031441460299875909588734720986560192536021217458484325625391881476254406473079046653046818198811063732807766626815778669059263539288279240724043002972198751108816706724514596508072044707863500473414019828271440565021291938453587422416281612723545945938909968678247193364858445334012215555435275427943811594957345986593699556195903066794743184472440265626440142038293478191736570249215 2048)) ?v_12) (bvlshr (bvand ?v_11 (_ bv32317006071311007298962968279132820423318564169544585575840362784271006144270719271112334871465990491032121249854708136351097131222229533897039842809000575024469795858601452903608286950487291036173656424642694699111215656720330692156806652878176294560992911131049744850351554674082581482982160517647675979048835286736621524221873911053756802868040397366267058518789526418606983189736261563041441886139662520217871559010598356884184331324030205339382405674779699808810844071987274263786247133048684130104820097246644482379610721840409187043258179179795737779347699068638486420172878212978512006155262375419323025981440 2048)) ?v_12))) (?v_14 ((_ zero_extend 2037) (_ bv128 11)))) (let ((?v_15 (bvor (bvshl (bvand ?v_13 (_ bv94971145180789141405469863695884969990413375523057264366393133656667101213790966126577778796192435976493286721619611273819053280153830754471864219391289063009512806159964370817305614238014244837688992683186106238684767551483551350234458097273324874897360483666819816039560925245068139788358907078031552764684530246952389718316880392918374272991258975094057996680343827463235688502168934277549034830891396697676020193061348779341148892066948388025097854535507810266613457395028123006836137017554784880056507653590091639305530513408919664906739868441072650790136656884348974268415 2048)) ?v_14) (bvlshr (bvand ?v_13 (_ bv32317006071311007300714876688669951960349131524534694890724875563828770168877477517674144147156520330032050859708107053367541780354298485118594865664828671846811824087147165337278333530998363043786544832224103197459486604404605511324149101655290064231896878300552753692653117794267740933710191915457110569482353408144600202632326067708533016730171645788373932339760925266412651919717201339056200596183833289262707915216292923080049316321410249206727677420171938451885976792643871821700059247191423513203065085185628574928209860250798213758159017512799345696238071622024309939738578610163879497403419196726710621962240 2048)) ?v_14))) (?v_16 ((_ zero_extend 2037) (_ bv256 11)))) (let ((?v_17 (bvor (bvshl (bvand ?v_15 (_ bv279095111627852376407822673918065072905887935345660252615989519488029661278602584477274180335287279405243496479269655964121202716886217624945655141584838007703178109579584255207605922065345056860944776274180728348556737279454388833698212982515973506422648097610271573739270676850754346538118912161587565627322601608861055814126836611515444383335727234678394072087732734025567668896419351136825388822676270715092663370710364205902957257037840983601227613820869153236869843656264309782139126643440567491781248474770930966086857614467652386815 2048)) ?v_16) (bvlshr (bvand ?v_15 (_ bv32317006071311007300714876688669951960444102669715484032130345427524655138867611798085573559146505641014799895848992131558773898897874931575600122725169680536153603186965708812344954253910382450831936435667181350651846563501034918154134916228896586215374039929970959986026631115266885080258995661844475996688216120407152368914262326688954297921116905358475567711539686747169438627081137712541397537050050280114428159335126130122919957080213913170378129944336867880090300295888143939010064438356220959263775585323618856951444769654532129484978655322733173025761463008789789037153537230130181217227468995996591943843840 2048)) ?v_16))) (?v_18 ((_ zero_extend 2037) (_ bv512 11)))) (let ((?v_19 (bvor (bvshl (bvand ?v_17 (_ bv2410312426921032588580116606028314112912093247945688951359675039065257391591803200669085024107346049663448766280888004787862416978794958324969612987890774471685899853150034451840262999015208137879147648906730546627516188125228793608498254413622185557461794521228420806236115696491848613995171671120355230896257999149258109674668529734341363050113939500588541302086847006769686052748707136868564708653190246324172185170594217116133658727496874721447108785121263615 2048)) ?v_18) (bvlshr (bvand ?v_17 (_ bv32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448280710318450446268407511633591722075539194702809692695116208601753153385228164358637425253452063124531982403270024154882788029124087013649227429510942494747442647489815192386233134523565554286718296887677415327531178143142900963914851815895844970678619654931422375297655621241901859303687650732732577258002390973227976426601145541195422760363881209530177954039354611088039227582300249931078656601680784145297277963248059010428202344946224651318834406502274474967040 2048)) ?v_18))) (?v_20 ((_ zero_extend 2037) (_ bv1024 11)))) (let ((?v_21 (bvor (bvshl (bvand ?v_19 (_ bv179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137215 2048)) ?v_20) (bvlshr (bvand ?v_19 (_ bv32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521734564076182110829912044267485667021494378337432091400804375578173293516902959351017550115541769580704823489838590463999939561383487229281910850182593813106849357791285954724448854882125685229350225459628571692166207846586010535756741612055848610098380251624748643306405371232666472431888720497281435372093440 2048)) ?v_20)))) (let ((?v_22 (bvor (bvshl (bvand ?v_21 (_ bv10772335357103669100238292229556650653481367556571828010710115142508218379622630297732400470507637821229572653640632673164706519716830307031696050795482761040210292455766998697250065916796550702265352546128022522758930739547539918720612698112825390156860548617345435014295858630513688602869184133041310128507304777796556114140228324928854856498285392011775440686025935219777008730902820104716752864288059038908647867906153952452532783717433881968134565871077762410409041894903606736575052367242310441156559514193552232645015332422784332879405175055463145778514534045144409868215106159534984049397851951203686532076885 2048)) ?v_0) (bvlshr (bvand ?v_21 (_ bv21544670714207338200476584459113301306962735113143656021420230285016436759245260595464800941015275642459145307281265346329413039433660614063392101590965522080420584911533997394500131833593101404530705092256045045517861479095079837441225396225650780313721097234690870028591717261027377205738368266082620257014609555593112228280456649857709712996570784023550881372051870439554017461805640209433505728576118077817295735812307904905065567434867763936269131742155524820818083789807213473150104734484620882313119028387104465290030664845568665758810350110926291557029068090288819736430212319069968098795703902407373064153770 2048)) ?v_0)))) (let ((?v_23 (bvor (bvshl (bvand ?v_22 (_ bv6463401214262201460142975337733990392088820533943096806426069085504931027773578178639440282304582692737743592184379603898823911830098184219017630477289656624126175473460199218350039550077930421359211527676813513655358443728523951232367618867695234094116329170407261008577515178308213161721510479824786077104382866677933668484136994957312913898971235207065264411615561131866205238541692062830051718572835423345188720743692371471519670230460329180880739522646657446245425136942164041945031420345386264693935708516131339587009199453670599727643105033277887467108720427086645920929063695720990429638711170722211919246131 2048)) ?v_2) (bvlshr (bvand ?v_22 (_ bv25853604857048805840571901350935961568355282135772387225704276342019724111094312714557761129218330770950974368737518415595295647320392736876070521909158626496504701893840796873400158200311721685436846110707254054621433774914095804929470475470780936376465316681629044034310060713232852646886041919299144308417531466711734673936547979829251655595884940828261057646462244527464820954166768251320206874291341693380754882974769485886078680921841316723522958090586629784981700547768656167780125681381545058775742834064525358348036797814682398910572420133111549868434881708346583683716254782883961718554844682888847676984524 2048)) ?v_2)))) (let ((?v_24 (bvor (bvshl (bvand ?v_23 (_ bv1901000357135941605924404511098232468261417804100910825419432083972038537580464170188070671266053733158159880054229295264359974067675936535005185434496957830625345727488293887750011632375861888635062214022592209898634836390742338597755182019910362968857743873649194414287504464208297988741620729360231199148347901964098137789452057340386151146756245649136842474004576803490060364276968253773544623109657477454467270806968344550446961832488332112023746918425487484189830922630048247630891594219231254321745796622391570466767411604020764625777383833317025725620211890319601741449724616388526596952562109035944682131215 2048)) ?v_4) (bvlshr (bvand ?v_23 (_ bv30416005714175065694790472177571719492182684865614573206710913343552616601287426723009130740256859730530558080867668724229759585082814984560082966951951325290005531639812702204000186118013790218160995424361475358378157382251877417564082912318565807501723901978387110628600071427332767819865931669763699186373566431425570204631232917446178418348099930386189479584073228855840965828431492060376713969754519639271476332911493512807151389319813313792379950694807799747037294762080771962094265507507700069147932745958265127468278585664332234012438141333072411609923390245113627863195593862216425551240993744575114914099440 2048)) ?v_4)))) (let ((?v_25 (bvor (bvshl (bvand ?v_24 (_ bv125747105335840495333520920967587361713790282761538848374048036682975311824388680518277048293863476512407462882964583733440153926655606696868047285550382424593894464464206210473736178017080358392202558904218161744267674002500465977283416709488234126344675664793915583824465275842572240500418491825384943134326514915913106390741964882437994433832125198581036272599524535639420335380188561533658593746553218353019235812134092830185207592032302124141648628845265709070922668033894242061187381718781833943461784212376096100914575864857404663961928113487896643328963432433592333092005130266945339098029400208603344732415 2048)) ?v_6) (bvlshr (bvand ?v_24 (_ bv32191258965975166805381355767702364598730312386953945183756297390841679827043502212678924363229049987176310498038933435760679405223835314398220105100897900696036982902836789881276461572372571748403855079479849406532524544640119290184554677628987936344236970187242389459063110615698493568107133907298545442387587818473755236029943009904126575061024050836745285785478281123691605857328271752616599999117623898372924367906327764527413143560269343780262048984388021522156203016676925967663969720008149489526216758368280601834131421403495593974253597052901540692214638702999637271553313348338006809095526453402456251498240 2048)) ?v_6)))) (let ((?v_26 (bvor (bvshl (bvand ?v_25 (_ bv493110854499153261527303304830400414429163719268741078049504027152977022733232996524058187154171131783400490729235363527383303464462683996751272600003788441958449080173047226631524142856549004482903667216748822318336088295811827763886630366639854898310597766941366022901377479767781036797649456019102650190303406219229875374531714524414675213922763874381285717351691497311915806227145891849646132610039780837175085886117183535370834050266286920432789075075656304548989512561008593767263638886841499053506851741469043409601385435225185752143301114887612147878963061101869624862983024529730566675214853496666914815 2048)) ?v_8) (bvlshr (bvand ?v_25 (_ bv32316512960456508147453349385365121560029673505996215291052295923497502161845157660200677353335759292556934560431168784130592175847026458411091401113848279332188918918220823044523566226246795557791574734716850819454473882554323944334074207708109530615683335254269363676864674514061298027570754749667911282871724029983449112545310443072040154819642253271451940772360453967833714276902233168258408946731567076945106428632575740174062980318251379617483264824158211574922576695198259201131389838088044481970625035728915228891636395882917773452463381865274549723395723172372127735020455495580422417626880638757562929315840 2048)) ?v_8)))) (let ((?v_27 (bvor (bvshl (bvand ?v_26 (_ bv7524389322797446040883062092537733229786709286255942365591042456667314442386984930096710212860769417795340657030827683038844698134727362301284631268392235937583875243951827485067390432889168540459798904583851961347493402961438138317409892571406969311454956545629852567160903318873644454808418626039175260691609949036049282500668357192980174976837821551246685093927923721588007749784843196246171229662840693970933302712516988312146012401244517765743466989949769396632294237631961231141629598705401114366081875798891955552658541527505604808849729680814712227957530391280469301474478369841928076546552539119615 2048)) ?v_10) (bvlshr (bvand ?v_26 (_ bv32317006063786617977917430647786889867906369439928774745874403061933612682200576450810216481426203250827948543126557362463291876111646222960360790085163651852238641429717120847798370265322261673906889097924268663692940257295126353200399956021066277899174676540581348497257723324380162489733907944315511759482739072698058393384635692285896212301876001058488500506831120565403102471120452564365415396618005887063102909747528554645081362840155633503159179847489820241277356288078525972093195870585301724764277428214574822136154041715694457110709920357539707654728889907475699213364849177130473778351627777064507057111040 2048)) ?v_10)))) (let ((?v_28 (bvor (bvshl (bvand ?v_27 (_ bv1751908409537131537125538500170898456289982643253648994597171622084866540056922972656596711067189883143022427928261387198048309577447708096161081508699543188141910799902361070622401213741372869165576561922289064005031441460299875909588734720986560192536021217458484325625391881476254406473079046653046818198811063732807766626815778669059263539288279240724043002972198751108816706724514596508072044707863500473414019828271440565021291938453587422416281612723545945938909968678247193364858445334012215555435275427943811594957345986593699556195903066794743184472440265626440142038293478191736570249215 2048)) ?v_12) (bvlshr (bvand ?v_27 (_ bv32317006071311007298962968279132820423318564169544585575840362784271006144270719271112334871465990491032121249854708136351097131222229533897039842809000575024469795858601452903608286950487291036173656424642694699111215656720330692156806652878176294560992911131049744850351554674082581482982160517647675979048835286736621524221873911053756802868040397366267058518789526418606983189736261563041441886139662520217871559010598356884184331324030205339382405674779699808810844071987274263786247133048684130104820097246644482379610721840409187043258179179795737779347699068638486420172878212978512006155262375419323025981440 2048)) ?v_12)))) (let ((?v_29 (bvor (bvshl (bvand ?v_28 (_ bv94971145180789141405469863695884969990413375523057264366393133656667101213790966126577778796192435976493286721619611273819053280153830754471864219391289063009512806159964370817305614238014244837688992683186106238684767551483551350234458097273324874897360483666819816039560925245068139788358907078031552764684530246952389718316880392918374272991258975094057996680343827463235688502168934277549034830891396697676020193061348779341148892066948388025097854535507810266613457395028123006836137017554784880056507653590091639305530513408919664906739868441072650790136656884348974268415 2048)) ?v_14) (bvlshr (bvand ?v_28 (_ bv32317006071311007300714876688669951960349131524534694890724875563828770168877477517674144147156520330032050859708107053367541780354298485118594865664828671846811824087147165337278333530998363043786544832224103197459486604404605511324149101655290064231896878300552753692653117794267740933710191915457110569482353408144600202632326067708533016730171645788373932339760925266412651919717201339056200596183833289262707915216292923080049316321410249206727677420171938451885976792643871821700059247191423513203065085185628574928209860250798213758159017512799345696238071622024309939738578610163879497403419196726710621962240 2048)) ?v_14)))) (let ((?v_30 (bvor (bvshl (bvand ?v_29 (_ bv279095111627852376407822673918065072905887935345660252615989519488029661278602584477274180335287279405243496479269655964121202716886217624945655141584838007703178109579584255207605922065345056860944776274180728348556737279454388833698212982515973506422648097610271573739270676850754346538118912161587565627322601608861055814126836611515444383335727234678394072087732734025567668896419351136825388822676270715092663370710364205902957257037840983601227613820869153236869843656264309782139126643440567491781248474770930966086857614467652386815 2048)) ?v_16) (bvlshr (bvand ?v_29 (_ bv32317006071311007300714876688669951960444102669715484032130345427524655138867611798085573559146505641014799895848992131558773898897874931575600122725169680536153603186965708812344954253910382450831936435667181350651846563501034918154134916228896586215374039929970959986026631115266885080258995661844475996688216120407152368914262326688954297921116905358475567711539686747169438627081137712541397537050050280114428159335126130122919957080213913170378129944336867880090300295888143939010064438356220959263775585323618856951444769654532129484978655322733173025761463008789789037153537230130181217227468995996591943843840 2048)) ?v_16)))) (let ((?v_31 (bvor (bvshl (bvand ?v_30 (_ bv2410312426921032588580116606028314112912093247945688951359675039065257391591803200669085024107346049663448766280888004787862416978794958324969612987890774471685899853150034451840262999015208137879147648906730546627516188125228793608498254413622185557461794521228420806236115696491848613995171671120355230896257999149258109674668529734341363050113939500588541302086847006769686052748707136868564708653190246324172185170594217116133658727496874721447108785121263615 2048)) ?v_18) (bvlshr (bvand ?v_30 (_ bv32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448280710318450446268407511633591722075539194702809692695116208601753153385228164358637425253452063124531982403270024154882788029124087013649227429510942494747442647489815192386233134523565554286718296887677415327531178143142900963914851815895844970678619654931422375297655621241901859303687650732732577258002390973227976426601145541195422760363881209530177954039354611088039227582300249931078656601680784145297277963248059010428202344946224651318834406502274474967040 2048)) ?v_18)))) (not (= (bvnot (ite (= (bvor (bvshl (bvand ?v_31 (_ bv179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137215 2048)) ?v_20) (bvlshr (bvand ?v_31 (_ bv32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521734564076182110829912044267485667021494378337432091400804375578173293516902959351017550115541769580704823489838590463999939561383487229281910850182593813106849357791285954724448854882125685229350225459628571692166207846586010535756741612055848610098380251624748643306405371232666472431888720497281435372093440 2048)) ?v_20)) x) (_ bv1 1) (_ bv0 1))) (_ bv0 1))))))))))))))))))))))))))
(check-sat)
(exit)
